Lemma auto_proof:
  forall p q: Prop, (p->q) -> ~q -> ~p.
Proof.
  auto.
Qed.